T:Type. T    (bs, as:T List, x:T. (x  merge(as;bs))  (x  as)  (x  bs)) 

latex

Definitions	(x  l), P  Q, x:A. B(x), False, t  T, Prop, P  Q, merge(as;bs), P  Q, P & Q, P  Q, x. t(x), s-insert(x;l), {T}
Lemmas	nil member, member-s-insert, s-insert wf, all functionality wrt iff, iff functionality wrt iff, or functionality wrt iff, cons member, false wf, iff wf, merge wf, l member wf